/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]

␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206  ␈↓ βiRECURSIVE PROGRAMMING AND PROVING ␈↓ 
0FALL 1979
␈↓ ↓H␈↓␈↓ ¬DPROBLEM SET  2
␈↓ ↓H␈↓␈↓ ¬uDue  Oct. 29


␈↓ ↓H␈↓αMore about append.

␈↓ ↓H␈↓1.  Prove the following cancellation rules for ␈↓↓append:␈↓

␈↓ ↓H␈↓1.1. ∀u v w:[ [u*w=v*w]≡[u=v] ]
␈↓ ↓H␈↓1.2. ∀u v w:[ [w*u=w*v]≡[u=v] ]


␈↓ ↓H␈↓αRightwing lists.

␈↓ ↓H␈↓2.␈α
 Recall␈α∞that␈α
when␈α∞restricted␈α
to␈α∞lists␈α
the␈α
operations␈α∞␈↓↓car,␈↓␈α
␈↓↓cdr␈↓␈α∞and␈α
␈↓↓cons␈↓␈α∞behave␈α
unsymmetrically.
␈↓ ↓H␈↓␈↓ ↓xThus␈αit␈αis␈αeasy␈αto␈αget␈αthe␈αfirst␈α(left␈αmost)␈αelement␈αof␈αa␈αlist␈αand␈αthe␈αrest␈αof␈αthe␈αlist.␈α  Often␈αone
␈↓ ↓H␈↓␈↓ ↓xwould like to work on the other end of a list.

␈↓ ↓H␈↓2.1.␈α Write␈αprograms␈αto␈αcompute␈αthe␈αfunctions␈α␈↓↓rac,␈↓␈α␈↓↓rdc␈↓␈αand␈α␈↓↓snoc,␈↓␈αwhere␈αfor␈αnon-empty␈αlists␈α␈↓↓uu,␈↓
␈↓ ↓H␈↓␈↓ ↓x␈↓↓rac[uu]␈↓␈αis␈αthe␈αlast␈αelement,␈α␈↓↓rdc[uu]␈↓␈αis␈αthe␈αlist␈αobtained␈αby␈αremoving␈αthe␈αlast␈αelement,␈αand␈αfor␈αa
␈↓ ↓H␈↓␈↓ ↓xlist␈α␈↓↓u,␈↓␈αand␈αan␈αS-expression␈α␈↓↓x,␈↓␈α␈↓↓snoc[u,x]␈↓␈αadds␈α␈↓↓x␈↓␈αto␈αthe␈αend␈αof␈αthe␈αlist␈α␈↓↓u.␈↓␈α Use␈αonly␈α␈↓↓car,␈↓␈α␈↓↓cdr,␈↓
␈↓ ↓H␈↓␈↓ ↓x␈↓↓cons␈↓ and recursive defintion.

␈↓ ↓H␈↓2.2.  Give axioms characterizing the functions ␈↓↓rac,␈↓ ␈↓↓rdc␈↓ and ␈↓↓snoc␈↓ representing your programs.

␈↓ ↓H␈↓The functions ␈↓↓rac,␈↓ ␈↓↓rdc,␈↓ ␈↓↓snoc␈↓ have the following properties

␈↓ ↓H␈↓␈↓ αH  (i)  ␈↓↓rac␈↓ of a non-empty list is an S-expression,
␈↓ ↓H␈↓␈↓ αH (ii)  ␈↓↓rdc␈↓ of a non-empty list is an list,
␈↓ ↓H␈↓␈↓ αH(iii)  ␈↓↓snoc␈↓ of a list and an S-expression is a non-empty list,
␈↓ ↓H␈↓␈↓ αH (iv)   the ␈↓↓rac␈↓ of the ␈↓↓snoc␈↓ of a list, ␈↓↓u,␈↓  and an S-expression, ␈↓↓x,␈↓ is ␈↓↓x,␈↓
␈↓ ↓H␈↓␈↓ αH  (v)   the ␈↓↓rdc␈↓ of the ␈↓↓snoc␈↓ of a list, ␈↓↓u,␈↓  and an S-expression, ␈↓↓x,␈↓ is ␈↓↓u,␈↓ and
␈↓ ↓H␈↓␈↓ αH (vi)   for a non-empty list ␈↓↓uu,␈↓ ␈↓↓snoc␈↓ of the ␈↓↓rdc␈↓ and the ␈↓↓rac␈↓ of ␈↓↓uu␈↓ is just ␈↓↓uu.␈↓

␈↓ ↓H␈↓2.3.␈α
 Give␈α
domain/range␈α
specifications␈α
and␈α
axioms␈α
formallizing␈α
the␈α
above␈α
properties␈α
of␈α
␈↓↓rac,␈↓␈α␈↓↓rdc␈↓
␈↓ ↓H␈↓␈↓ ↓xand ␈↓↓snoc.␈↓

␈↓ ↓H␈↓2.4.␈α Prove␈α
that␈αyour␈αprograms␈α
satisfy␈αthese␈α
specifications␈α(using␈αthe␈α
axioms␈αfor␈αthe␈α
representation
␈↓ ↓H␈↓␈↓ ↓xof the programs as functions).


␈↓ ↓H␈↓αSplitting lists.

␈↓ ↓H␈↓3.␈α∂ A␈α∂pair␈α∂of␈α∂lists␈α∂␈↓↓[v . w]␈↓␈α∂is␈α∂said␈α∂to␈α∞split␈α∂a␈α∂list␈α∂␈↓↓u␈↓␈α∂(␈↓↓Issplit[v,w,u]␈↓)␈α∂if␈α∂␈↓↓v*w=u␈↓.␈α∂ Write␈α∂a␈α∞program
␈↓ ↓H␈↓␈↓ ↓x␈↓↓splits[u]␈↓␈α
that␈αcomputes␈α
a␈αlist␈α
containing␈α
exactly␈αthose␈α
pairs␈αof␈α
lists␈α
that␈αsplit␈α
the␈αlist␈α
␈↓↓u.␈↓␈α Give␈α
a
␈↓ ↓H␈↓␈↓ ↓xsentence␈αthat␈αdefines␈αthe␈αrelation␈α␈↓↓Allsplits[w,u],␈↓␈αcharacterizing␈αthe␈αlist␈α␈↓↓w␈↓␈αof␈αall␈αsplits␈αof␈αa␈αlist
␈↓ ↓H␈↓␈↓ ↓x␈↓↓u␈↓ and show that your program is correct with respect to this specification.